Nuprl Lemma : es-snds_wf
11,40
postcript
pdf
the_es
:ES,
l
:IdLnk,
e
:E. snds(
l
;before(
e
))
((Msg on
l
) List)
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
snds(
l
;before(
e
))
Lemmas
concat
wf
,
es-Msgl
wf
,
map
wf
,
es-E
wf
,
es-sends
wf
,
es-before
wf
,
IdLnk
wf
,
event
system
wf
origin
the_es:ES, l:IdLnk, e:E. snds(l;before(e)) 
((Msg on l) List) the_es:ES, l:IdLnk, e:E. snds(l;before(e)) ((Msg on l) List) x:A. B(x) T